/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */

package ch.epfl.lara.patterns.test;

import ch.epfl.lara.patterns.ast._
import ch.epfl.lara.patterns.analyze.Verifier._
import ch.epfl.lara.patterns.analyze.HierarchyHolder
import ch.epfl.lara.patterns.utils._

import ch.epfl.lara.patterns.formdeciderwrapper.FormDeciderWrapper

import scala.collection.immutable.HashMap

object Main {
  
  private var verbose = false
	
  // Contains the klass definition for some of the primitive Scala type 
  val primitivesKlasses: Map[String,HierarchyKlass] = HashMap.empty + 
                           (("PrimitiveInt",HierarchyKlass(false,true,true,"PrimitiveInt", None, List())))
  
                           
  /**
   * Tree Hierarchy definition:
   * 
   *   abstract class Tree
   *   case class Node(left: Tree, v: PrimitiveInt, right: Int) extends tree
   *   case object EmptyTree extends Tree
   */
  val treeHierarchy: Map[String,HierarchyKlass] = primitivesKlasses + 
        (("Tree",HierarchyKlass(true,false,false,"Tree", None, List())) , 
        ("Node",HierarchyKlass(false,true, false,"Node",Some("Tree"),FieldDef("left","Tree") :: FieldDef("v","PrimitiveInt") :: FieldDef("right","Tree") :: Nil)),
        ("EmptyNode",HierarchyKlass(false, true, true,"EmptyNode",Some("Tree"), Nil)))
  

  /**
   * Arith Hierarchy definition:
   *
   *   abstract class Arith
   *   case class Sum(l: Arith, r: Arith) extends Arith
   *   case class Prod(n: Num, f: Arith) extends Arith
   *   case class Num(n: PrimitiveInt) extends Arith
   */
  val arithHierarchy: Map[String,HierarchyKlass] = primitivesKlasses + 
      (("Arith",HierarchyKlass(true,false,false,"Arith", None, List())) , 
      ("Sum",HierarchyKlass(false,true, false,"Sum",Some("Arith"),FieldDef("l","Arith") :: FieldDef("r","Arith") :: Nil)),
      ("Prod",HierarchyKlass(false, true, false,"Prod",Some("Arith"), FieldDef("n","Num") :: FieldDef("f","Arith") :: Nil)),
      ("Num",HierarchyKlass(false, true, false,"Num",Some("Arith"), FieldDef("n","PrimitiveInt") :: Nil))
      )     
      
  
  // Ready-to-use build functions. The hierarchy is already specified.
  
  def buildArith(selector: (String, String), patterns: List[Pattern]) = buildTest(arithHierarchy)(selector,patterns)  
  
  def buildTree(selector: (String, String), patterns: List[Pattern]) = buildTest(treeHierarchy)(selector,patterns)  
  
  def buildPrimitives(selector: (String, String), patterns: List[Pattern]) = buildTest(primitivesKlasses)(selector,patterns)  
  
  
  def main (args: Array[String]): Unit = {
    if(args.length >= 1 && args(0).contains("-v"))
      verbose = true
	  
    setFormulaDecider(FormDeciderWrapper)
	
    // Example 1: Test pattern matching on int primitive type
    testInteger
    
    // Example 2: Test pattern matching on a classical Tree structure
    testTreeNodeExample    
    
    // Exaample 3: Test pattern matching on the example gave for the presentation
    testExamplePresentation
    
    
    // Some examples that goes wrong (just to show that we don't just output VALID :) )
    
    Console.println("The following test should fail completeness but succeed disjointness\n")
    
    testTreeNodeNotComplete
    
    Console.println("The following test should succeed completeness but fail disjointness\n")
    
    testExamplePresentationNotDisjoint
  }
  
  /**
   * A simple pattern matching expression on integer
   *
   * t match {
   *   case v: PrimitiveInt if (v == 0) => ..
   *   case v: PrimitiveInt if (v != 0) => ..
   * }
   *
   * Clearly the test must generate formulae that are both complete and disjoint
   */
  def testInteger = {
    val selector = ("t", "PrimitiveInt")
    
    val patterns =  GuardedKlass(SimpleArgument("v","PrimitiveInt"),Assume(LessEq(Var("v"),IntValue(0)))) ::
    GuardedKlass(SimpleArgument("v","PrimitiveInt"),Assume(Less(IntValue(0),Var("v")))) :: Nil
    
    buildPrimitives(selector,patterns)
  }
  
  
  /**
   * A simple pattern matching on the tree:
   *
   *   t match {
   *     case Node(left: Tree, v: PrimitiveInt, right: Tree) if (v == 3) => ...
   *	 case Node(left: Tree, v: PrimitiveInt, right: Tree) if (v != 3) => ...
   *     case EmptyTree => ...
   *   }
   * 
   * Clearly the test must generate formulae that are complete and disjoint
   *
   */
    def testTreeNodeExample = {
    val selector = ("t", "Tree")
    
    val patterns =  GuardedKlass(Klass("Node", SimpleArgument("left", "Tree") :: SimpleArgument("v","PrimitiveInt") :: 
                                               SimpleArgument("right", "Tree") :: Nil),Assume(Equal(Var("v"),IntValue(3)))) ::
                    GuardedKlass(Klass("Node", SimpleArgument("left", "Tree") :: SimpleArgument("v","PrimitiveInt") :: 
                                               SimpleArgument("right", "Tree") :: Nil),Assume(Not(Equal(Var("v"),IntValue(3))))) :: 
                    Objekt("EmptyNode") :: Nil

    buildTree(selector,patterns)
  }

   /**
    * A more complicated pattern matchng whose we could suppose to be complete, but it's not the case...
    *
    *   t match {
    *     case Node(left: Node, v: PrimitiveInt, right: Tree) if (v == 3) => ...
    *     case Node(left: Tree, v: PrimitiveInt, right: EmptyNode) if (v != 3) => ...
    *     case Node(left: EmptyNode, v: PrimitiveInt, right: Node) => ...
    *     case EmptyTree => ...
    *   }
    * 
    *  Not complete but disjoint
    *
    */
   def testTreeNodeNotComplete = {
     val selector = ("t", "Tree")
     
     val patterns =  GuardedKlass(Klass("Node", SimpleArgument("left", "Node") :: SimpleArgument("v","PrimitiveInt") :: 
                                                SimpleArgument("right", "Tree") :: Nil),Assume(Equal(Var("v"),IntValue(3)))) ::
                     GuardedKlass(Klass("Node", SimpleArgument("left", "Node") :: SimpleArgument("v","PrimitiveInt") :: 
                                                SimpleArgument("right", "EmptyNode") :: Nil),Assume(Not(Equal(Var("v"),IntValue(3))))) :: 
                     Klass("Node", SimpleArgument("left", "EmptyNode") :: SimpleArgument("v","PrimitiveInt") :: 
                                                    SimpleArgument("right", "Node") :: Nil) ::                                                
                     Objekt("EmptyNode") :: Nil

     buildTree(selector,patterns)
   }
    

   /**
    * A simple pattern matching on arithmetics (could be an evaluator):
    * 
    *   t match {
    *	  case Sum(l: Arith, r: Arith) =>
    *     case Prod(Num(n: PrimitiveInt), f: Arith) if (n == 0) => ...
    *     case Prod(Num(n: PrimitiveInt), f: Arith) if (n != 0) => ...
    *     case Num(n: PrimitiveInt) => ...
    *   }
    * 
    * Clearly the test must generate formulae that are complete and disjoint
    *
    */
  def testExamplePresentation = {
    val selector = ("t", "Arith")
    
    val patterns =  Klass("Sum", SimpleArgument("l","Arith") :: SimpleArgument("r","Arith") :: Nil) ::
    		GuardedKlass(Klass("Prod", Klass("Num", SimpleArgument("n","PrimitiveInt") :: Nil) :: SimpleArgument("f","Arith") :: Nil), Assume(Equal(Var("n"),IntValue(0)))) ::
                GuardedKlass(Klass("Prod", Klass("Num", SimpleArgument("n","PrimitiveInt") :: Nil) :: SimpleArgument("f","Arith") :: Nil),Assume(Not(Equal(Var("n"),IntValue(0))))) ::                    
                Klass("Num", Wildcard :: Nil) ::
       		Nil
                       
     
    buildArith(selector,patterns)
  }
  
  /**
   *  A simple pattern matching that is not disjoint (Prod(0,_) is atteinable by two 
   *	different patterns...the first will be always triggered since the sequential nature of pattern matching in Scala) :
   * 
   *   t match {
   *     case Sum(l: Arith, r: Arith) =>
   *     case Prod(Num(n: PrimitiveInt),_) if (0 <= n) => ...
   *     case Prod(Num(n: PrimitiveInt),_) if (n <= 0) => ...
   *     case Num(_) => ...
   *   }
   * 
   * Complete but not disjoint (because of the overlapping Prod patterns)
   *
   */
  def testExamplePresentationNotDisjoint = {
    val selector = ("t", "Arith")
    
    val patterns =  Klass("Sum", SimpleArgument("l","Arith") :: SimpleArgument("r","Arith") :: Nil) ::
                    GuardedKlass(Klass("Prod", Klass("Num", SimpleArgument("n","PrimitiveInt") :: Nil) ::Wildcard :: Nil),Assume((LessEq(IntValue(0),Var("n"))))) ::                    
                    GuardedKlass(Klass("Prod", Klass("Num", SimpleArgument("n","PrimitiveInt") :: Nil) :: Wildcard :: Nil),Assume((LessEq(Var("n"),IntValue(0))))) ::                    
                    Klass("Num", Wildcard :: Nil) ::
                       Nil
                       
     
    buildArith(selector,patterns)
  }
  
  /**
   * build the test 
   *
   */
  def buildTest(hierarchy: Map[String, HierarchyKlass])(selector: (String, String), patterns: List[Pattern]) = {
    
    var matsch = Match(selector,patterns)   
    
    if(verbose) Console.println("Before Renaming")
    
    Console.println(matsch)
    
    matsch = FreshRenamer(matsch)
    
    if(verbose) {
      Console.println("After Renaming")
      Console.println(matsch)
    }
  
    //val env = new HierarchyHolder(arithHierarchy)
    test(new HierarchyHolder(hierarchy),matsch)
  }
    
  /**
   * test:
   *    1- build formulae
   *    2- verify completeness and disjointness of the pttern matching expression
   */
  def test(env: Env, matsch: Match): Unit = {
    // 1- build formulae
    val form = buildCompletenessFormula(env,matsch)
    val form2 = buildDisjointnessFormula(env,matsch)

    if(verbose) {
      Console.println("Completeness formula")
      Console.println("********************")
      Console.println(form) 
      Console.println
      Console.println

      Console.println("Disjointness formula")
      Console.println("********************")
      Console.println(form2) 
    }
	  
    // 2- Test completeness and disjointness
    Console.print("And this is ...")
    Console.println(if(isComplete(env,matsch)) "complete !" else "not complete :(")
    Console.print("And this is ...")
    Console.println(if(isDisjoint(env,matsch)) "disjoint !" else "overlapping :(")
    Console.println
    Console.println
  }
}



